Nuprl Definition : mul_mon_of_rng
13,42
postcript
pdf
r
xmn == <|
r
|, =
,
, *, 1,
z
.
z
>
latex
clarification:
r
xmn == <|
r
|, =
r
,
r
, *
r
, 1
r
,
z
.
z
>
latex
Up
rings
1
Wellformedness Lemmas
mul
mon
of
rng
wf
,
mul
mon
of
rng
wf
c
,
mul
mon
of
rng
wf
a
,
mul
mon
of
rng
wf
b
Definitions
|
r
|
,
=
,
,
*
,
1
origin
xmn == <|r|, =
, 
, *, 1, 
z.z>
xmn == <|r|, =r, r, *r, 1r, z.z> xmn == <|r|, =, , *, 1, z.z>
xmn == <|r|, =r, r, *r, 1r, z.z>